A:es_realizer{i:l}, P:(ES{i}Prop{i'}).
(es:ES{i}. P(es))  R-Feasible{i:l}(A)  A ||-{i} es.P(es) 

latex

Definitions	t  T, x:A. B(x), ES, Consistent(R;es), f(a), x(s), P  Q, x:AB(x), R-Feasible(R), x:AB(x), P & Q, R ||- es.P(es), Realizer, Type, Prop
Lemmas	R-Feasible wf, es realizer wf, R-consistent wf, event system wf